The computability path ordering: the end of a quest
Identifieur interne : 003E48 ( Main/Exploration ); précédent : 003E47; suivant : 003E49The computability path ordering: the end of a quest
Auteurs : Frédéric Blanqui [République populaire de Chine] ; Jean-Pierre Jouannaud [France] ; Albert Rubio [Espagne]Source :
English descriptors
- mix :
Abstract
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 004C33
- to stream Hal, to step Curation: 004C33
- to stream Hal, to step Checkpoint: 003161
- to stream Main, to step Merge: 003F77
- to stream Main, to step Curation: 003E48
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">The computability path ordering: the end of a quest</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-85226" status="OLD"><idno type="RNSR">200921233V</idno><orgName>Formal Methods for Embedded Systems</orgName><orgName type="acronym">FORMES</orgName><desc><address><addrLine>Tsinghua University FIT Building Haidian District 100084 Beijing China</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/wiki/projects:formes:home</ref></desc><listRelation><relation active="#struct-25361" type="direct"></relation><relation active="#struct-11574" type="indirect"></relation><relation active="#struct-92114" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300133" type="indirect"></relation><relation active="#struct-300168" type="indirect"></relation><relation active="#struct-441569" type="indirect"></relation><relation active="#struct-86790" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-25361" type="direct"><org type="laboratory" xml:id="struct-25361" status="VALID"><orgName>Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées</orgName><orgName type="acronym">LIAMA</orgName><desc><address><addrLine>Institut d'Automatique - Académie des Sciences de Chine PO Box 2728 - Beijing 100080 R. P. Chine Tél. : (+ 86 10) 62 64 74 59 Fax : (+ 86 10) 62 64 74 58</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/</ref></desc><listRelation><relation active="#struct-11574" type="direct"></relation><relation active="#struct-92114" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300133" type="direct"></relation><relation active="#struct-300168" type="direct"></relation><relation active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-11574" type="indirect"><org type="institution" xml:id="struct-11574" status="VALID"><orgName>Centre de Coopération Internationale en Recherche Agronomique pour le Développement</orgName><orgName type="acronym">CIRAD</orgName><desc><address><addrLine>42, rue Scheffer 75116 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.cirad.fr</ref></desc></org></tutelle><tutelle active="#struct-92114" type="indirect"><org type="institution" xml:id="struct-92114" status="VALID"><orgName>Institut National de la Recherche Agronomique</orgName><orgName type="acronym">INRA</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inra.fr</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300133" type="indirect"><org type="institution" xml:id="struct-300133" status="VALID"><orgName>Chinese Academy of Science (CAS)</orgName><desc><address><country key="CN"></country></address></desc></org></tutelle><tutelle active="#struct-300168" type="indirect"><org type="institution" xml:id="struct-300168" status="VALID"><orgName>Institute of Automation, Chinese Academy of Sciences</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-86790" type="direct"><org type="laboratory" xml:id="struct-86790" status="VALID"><idno type="RNSR">196718247G</idno><orgName>INRIA Paris-Rocquencourt</orgName><desc><address><addrLine>INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex / INRIA Paris - 23 avenue d'Italie 75013 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/paris-rocquencourt</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>République populaire de Chine</country></affiliation></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-74848" status="VALID"><orgName>Llenguatges i Sistemes Informàtics</orgName><orgName type="acronym">LSI</orgName><desc><address><addrLine>Universitat Politécnica de Catalunya FIB / FME C/ Pau Gargallo 5, E-Barcelona 08028</addrLine><country key="ES"></country></address><ref type="url">http://www.lsi.upc.edu/</ref></desc><listRelation><relation active="#struct-85878" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-85878" type="direct"><org type="institution" xml:id="struct-85878" status="VALID"><orgName>Universitat Politècnica de Catalunya [Barcelona]</orgName><orgName type="acronym">UPC</orgName><desc><address><addrLine>Universitat Politècnica de Catalunya C. Jordi Girona, 31. 08034 Barcelona</addrLine><country key="ES"></country></address><ref type="url">http://www.upc.edu/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Espagne</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00288209</idno><idno type="halId">inria-00288209</idno><idno type="halUri">https://hal.inria.fr/inria-00288209</idno><idno type="url">https://hal.inria.fr/inria-00288209</idno><date when="2008-09-15">2008-09-15</date><idno type="wicri:Area/Hal/Corpus">004C33</idno><idno type="wicri:Area/Hal/Curation">004C33</idno><idno type="wicri:Area/Hal/Checkpoint">003161</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">003161</idno><idno type="wicri:Area/Main/Merge">003F77</idno><idno type="wicri:Area/Main/Curation">003E48</idno><idno type="wicri:Area/Main/Exploration">003E48</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">The computability path ordering: the end of a quest</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-85226" status="OLD"><idno type="RNSR">200921233V</idno><orgName>Formal Methods for Embedded Systems</orgName><orgName type="acronym">FORMES</orgName><desc><address><addrLine>Tsinghua University FIT Building Haidian District 100084 Beijing China</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/wiki/projects:formes:home</ref></desc><listRelation><relation active="#struct-25361" type="direct"></relation><relation active="#struct-11574" type="indirect"></relation><relation active="#struct-92114" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300133" type="indirect"></relation><relation active="#struct-300168" type="indirect"></relation><relation active="#struct-441569" type="indirect"></relation><relation active="#struct-86790" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-25361" type="direct"><org type="laboratory" xml:id="struct-25361" status="VALID"><orgName>Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées</orgName><orgName type="acronym">LIAMA</orgName><desc><address><addrLine>Institut d'Automatique - Académie des Sciences de Chine PO Box 2728 - Beijing 100080 R. P. Chine Tél. : (+ 86 10) 62 64 74 59 Fax : (+ 86 10) 62 64 74 58</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/</ref></desc><listRelation><relation active="#struct-11574" type="direct"></relation><relation active="#struct-92114" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300133" type="direct"></relation><relation active="#struct-300168" type="direct"></relation><relation active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-11574" type="indirect"><org type="institution" xml:id="struct-11574" status="VALID"><orgName>Centre de Coopération Internationale en Recherche Agronomique pour le Développement</orgName><orgName type="acronym">CIRAD</orgName><desc><address><addrLine>42, rue Scheffer 75116 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.cirad.fr</ref></desc></org></tutelle><tutelle active="#struct-92114" type="indirect"><org type="institution" xml:id="struct-92114" status="VALID"><orgName>Institut National de la Recherche Agronomique</orgName><orgName type="acronym">INRA</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inra.fr</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300133" type="indirect"><org type="institution" xml:id="struct-300133" status="VALID"><orgName>Chinese Academy of Science (CAS)</orgName><desc><address><country key="CN"></country></address></desc></org></tutelle><tutelle active="#struct-300168" type="indirect"><org type="institution" xml:id="struct-300168" status="VALID"><orgName>Institute of Automation, Chinese Academy of Sciences</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-86790" type="direct"><org type="laboratory" xml:id="struct-86790" status="VALID"><idno type="RNSR">196718247G</idno><orgName>INRIA Paris-Rocquencourt</orgName><desc><address><addrLine>INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex / INRIA Paris - 23 avenue d'Italie 75013 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/paris-rocquencourt</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>République populaire de Chine</country></affiliation></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-74848" status="VALID"><orgName>Llenguatges i Sistemes Informàtics</orgName><orgName type="acronym">LSI</orgName><desc><address><addrLine>Universitat Politécnica de Catalunya FIB / FME C/ Pau Gargallo 5, E-Barcelona 08028</addrLine><country key="ES"></country></address><ref type="url">http://www.lsi.upc.edu/</ref></desc><listRelation><relation active="#struct-85878" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-85878" type="direct"><org type="institution" xml:id="struct-85878" status="VALID"><orgName>Universitat Politècnica de Catalunya [Barcelona]</orgName><orgName type="acronym">UPC</orgName><desc><address><addrLine>Universitat Politècnica de Catalunya C. Jordi Girona, 31. 08034 Barcelona</addrLine><country key="ES"></country></address><ref type="url">http://www.upc.edu/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>Espagne</country></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>lambda-calculus</term><term>rewriting</term><term>term ordering</term><term>termination</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering.</div></front></TEI><affiliations><list><country><li>Espagne</li><li>France</li><li>République populaire de Chine</li></country></list><tree><country name="République populaire de Chine"><noRegion><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name></noRegion></country><country name="France"><noRegion><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></noRegion></country><country name="Espagne"><noRegion><name sortKey="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003E48 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003E48 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:inria-00288209
|texte= The computability path ordering: the end of a quest
}}
| This area was generated with Dilib version V0.6.33. |  |